|
|
Checking of Temporal Properties of Finite Traces of Programs
Sečkařová, Petra ; Češka, Milan (referee) ; Smrčka, Aleš (advisor)
Correct behavior of programs can be defined by their temporal properties. One of the options for formal specification of such properties is linear temporal logic - LTL . This master's thesis describes design and implementation of a tool for automatic checking of temporal properties of programs, that are specified using Past-Time LTL formulae. The trace of a given program is analyzed in run-time and any violation of given formulae is reported in details to help to find the code location with a root cause of the bug.
|
|
|
Runtime Verification of Systems with MTL Properties
Olšák, Ondřej ; Hruška, Martin (referee) ; Smrčka, Aleš (advisor)
This work is focused on the design of an algorithm for run-time verification over requirements given as formulas in metric temporal logic (MTL). Tree structure is used for verification of these requirements, which is similar to run of alternating timed automata from which the final algorithm is derivated. Designed algorithm is able to verify given MTL formulas over the runs of a program without a need to remember the whole program's trace. This allows to monitor a given program on potentially infinite runs.
|
|
|
Runtime Verification of Systems with MTL Properties
Olšák, Ondřej ; Hruška, Martin (referee) ; Smrčka, Aleš (advisor)
This work is focused on the design of an algorithm for run-time verification over requirements given as formulas in metric temporal logic (MTL). Tree structure is used for verification of these requirements, which is similar to run of alternating timed automata from which the final algorithm is derivated. Designed algorithm is able to verify given MTL formulas over the runs of a program without a need to remember the whole program's trace. This allows to monitor a given program on potentially infinite runs.
|
|
|
Checking of Temporal Properties of Finite Traces of Programs
Sečkařová, Petra ; Češka, Milan (referee) ; Smrčka, Aleš (advisor)
Correct behavior of programs can be defined by their temporal properties. One of the options for formal specification of such properties is linear temporal logic - LTL . This master's thesis describes design and implementation of a tool for automatic checking of temporal properties of programs, that are specified using Past-Time LTL formulae. The trace of a given program is analyzed in run-time and any violation of given formulae is reported in details to help to find the code location with a root cause of the bug.
|
guest ::
